\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
\usepackage{stmaryrd}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\fmu}[0]{ \mathbf{F}_{\omega}^{\mu}} 
\newcommand{\bred}[0]{\to_{\beta}} 
\newcommand{\rat}[0]{\rightarrowtail} 
\newcommand{\polym}[1]{\rightarrowtail_{#1}} 
\newcommand{\tyred}[0]{\to_{\tau}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

 
\begin{document}
%\pagestyle{empty}
\title{Strong Normalization for $\fmu$}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{\today}


\maketitle
\thispagestyle{empty}

\section{Specifications}

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Types} $T \ ::= \ X \ | \ \Pi X:\kappa.T \ | \ T_1 \to T_2 \ | \ \lambda X:\kappa.T \ | \ T_1 T_2 \ | \ \mu X.T$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \kappa' \to \kappa$. 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa $ 

\end{definition}


\begin{definition}[Well-formed Context]
\

\begin{tabular}{ll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

\end{tabular}

\end{definition}


\begin{definition}[Kinding]
\


\begin{tabular}{lll}
\infer[\textit{KVar}]{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&

\infer[\textit{Func}]{\Gamma \vdash T_1 \to T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma \vdash T_2 : *}

&

\infer[\textit{Poly}]{\Gamma \vdash \Pi X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : *}

\\
\\
\infer[\textit{TAbs}]{\Gamma \vdash \lambda X:\kappa.T: \kappa \to \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' }

&

\infer[\textit{TApp}]{\Gamma \vdash S T: \kappa}{\Gamma \vdash S: \kappa' \to \kappa & 
\Gamma \vdash T:\kappa'}
&

\infer[\textit{Mu}]{\Gamma \vdash \mu X. T : *}{ \Gamma, X:* \vdash T : *}


\end{tabular}

\end{definition}

\begin{definition}[Typing Rules]
\


\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \simeq_{\tau} T_2 & \Gamma \vdash T_2:*}

\\
\\
\infer[\textit{Func}]{\Gamma \vdash \lambda x.t :T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

&

\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

\\
\\

\infer[\textit{Gen}]{\Gamma \vdash t :\Pi X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X:\kappa.T 
& \Gamma \vdash T': \kappa}

\\
\\

\infer[\textit{unFold}]{\Gamma \vdash t:[\mu X.T/X]T}{\Gamma \vdash t: \mu X.T 
}

&

\infer[\textit{Fold}]{\Gamma \vdash t: \mu X.T}{\Gamma \vdash t: [\mu X.T/X]T && \Gamma \vdash \mu X.T:*}


\end{tabular}

\end{definition}

\begin{definition}[Type Reductions]
\

\begin{tabular}{llll}
  \infer{(\lambda X:\kappa.T)T' \tyred [T'/X]T }{}

&

  \infer{T T' \tyred T T'' }{ T' \tyred T''}

&
  \infer{T T' \tyred T'' T' }{ T \tyred T''}

&
  \infer{T \to T' \tyred T\to T'' }{ T' \tyred T''}

\\
\\

  \infer{T \to T' \tyred T''\to T' }{ T \tyred T''}

&
  \infer{\Pi X:\kappa. T \tyred \Pi X:\kappa. T' }{ T \tyred T'}

&
  \infer{ \lambda X:\kappa. T \tyred \lambda X:\kappa. T' }{ T \tyred T'}

  &
  
    \infer{ \mu X. T \tyred \mu X. T' }{ T \tyred T'}

\end{tabular}
\end{definition}

\begin{definition}[Term Reductions]
\

\begin{tabular}{llll}
  \infer{(\lambda x.t)t' \bred [t'/x]t }{}

&

  \infer{t t' \bred t t'' }{ t' \bred t''}

&
  \infer{t t' \bred t'' t' }{ t \bred t''}

&

  \infer{ \lambda x. t \bred \lambda x. t' }{ t \bred t'}

\end{tabular}
  
\end{definition}


\section{Strong Normalization}

\begin{definition}[Reducibility Candidate]
A reducibility candidate $\mathcal{R}$ is a set of terms such that: 
\begin{itemize}
\item If $t \in \mathcal{R}$, then $t$ is strongly normalisable.
\item If $t \in \mathcal{R}$ and $t \bred t'$, then $t'\in \mathcal{R}$.
  \item If $(\lambda x.t)t' \bred [t'/x]t$ with $[t'/x]t\in \mathcal{R}$, then $(\lambda x.t)t'\in \mathcal{R}$.
\end{itemize}
\end{definition}

Let $\mathfrak{R}$ be the set of all reducibility candidates. Let $\rho$ be a mapping between type variable to redicibility candidate. 
\begin{definition}
  \
  
  \begin{itemize}
  \item $\interp{*}_{\rho} := \mathfrak{R}$.
  \item $\interp{\kappa \to \kappa'}_{\rho} := \{ f \ | \ \forall a \in \interp{\kappa}_{\rho}, f(a) \in \interp{\kappa'}_{\rho} \}$.
  \item $\interp{X}_\rho := \rho(X)$. 
  \item $\interp{T_1 \to T_2}_{\rho} := \{ t \in \Lambda \ |\ \forall u.\in \interp{T_1}_{\rho}, tu \in \interp{T_2}_{\rho}\}$. 
  \item $\interp{\Pi X:\kappa.T}_{\rho} := \bigcap_{f \in \interp{\kappa}}\interp{T}_{\rho[f/X]}$. 
  \item $\interp{\mu X.T}_{\rho} := \mathrm{lfp}(f)$, where $f$ is a map $\mathcal{R} \mapsto \interp{T}_{\rho[\mathcal{R}/X]}$. 
  \item $\interp{\Lambda X:\kappa.T}_{\rho} := f$ where $f :  a \mapsto \interp{T}_{\rho[a/X]}$ for any $a \in \interp{\kappa}_{\rho}$. 
  \item $\interp{T_1 T_2}_{\rho} := \{ \interp{T_1}_{\rho}(a) \ | \ a \in \interp{T_2}_{\rho} \}$.
    
  \end{itemize}
\end{definition}

\begin{lemma}
  If $\Gamma \vdash T:*$, then $\interp{T}_{\rho}$ for $\Gamma \vdash \rho$. 
\end{lemma}
\begin{theorem}
If  $\Gamma \vdash t:T:*$, then $t \in \interp{T}_{\rho}$ and $\interp{T}_{\rho} \in \mathfrak{R}$ for $\Gamma \vdash \rho$. 
\end{theorem}

\end{document}
